<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>SearchTree: Binary Search Trees</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/vfa.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 3: Verified Functional Algorithms</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">SearchTree<span class="subtitle">Binary Search Trees</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 Binary search trees are an efficient data structure for
   lookup tables, that is, mappings from keys to values.
   The <span class="inlinecode"><span class="id" type="var">total_map</span></span> type from Maps.v is an <i>inefficient</i>
   implementation: if you add N items to your total_map,
   then looking them up takes N comparisons in the worst case,
   and N/2 comparisons in the average case.

<div class="paragraph"> </div>

   In contrast, if your <span class="inlinecode"><span class="id" type="var">key</span></span> type is a total order &mdash; that is,
   if it has a less-than comparison that's transitive and
   antisymmetric <span class="inlinecode"></span> <span class="inlinecode"><span class="id" type="var">a</span>&lt;<span class="id" type="var">b</span></span> <span class="inlinecode">↔</span>  <span class="inlinecode">~(<span class="id" type="var">b</span>&lt;<span class="id" type="var">a</span>)</span> <span class="inlinecode"></span> &mdash; then one can implement
   binary search trees (BSTs).   We will assume you know how BSTs
   work; you can learn this from:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Section 3.2 of  <i>Algorithms, Fourth Edition</i>,
       by Sedgewick and Wayne, Addison Wesley 2011;  or

</li>
<li> Chapter 12 of <i>Introduction to Algorithms, 3rd Edition</i>,
       by Cormen, Leiserson, and Rivest, MIT Press 2009.

</li>
</ul>
   Our focus here is to <i>prove the correctness of an implementation</i>
   of binary search trees. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Coq.Strings.String</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">VFA</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Perm</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">FunctionalExtensionality</span>.<br/>
</div>

<div class="doc">
<a name="lab59"></a><h1 class="section">Total and Partial Maps</h1>

<div class="paragraph"> </div>

 Recall the <span class="inlinecode"><span class="id" type="var">Maps</span></span> chapter of Volume 1 (Logical Foundations),
    describing functions from identifiers to some arbitrary type <span class="inlinecode"><span class="id" type="var">A</span></span>.
    VFA's <span class="inlinecode"><span class="id" type="var">Maps</span></span> module is almost exactly the same, except that it
    implements functions from <span class="inlinecode"><span class="id" type="var">nat</span></span> to some arbitrary type <span class="inlinecode"><span class="id" type="var">A</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="var">From</span> <span class="id" type="var">VFA</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
</div>

<div class="doc">
<a name="lab60"></a><h1 class="section">Sections</h1>

<div class="paragraph"> </div>

 We will use Coq's <span class="inlinecode"><span class="id" type="keyword">Section</span></span> feature to structure this development,
     so first a brief introduction to Sections.  We'll use the example
     of lookup tables implemented by lists. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">SectionExample1</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Definition</span> <span class="id" type="var">mymap</span> (<span class="id" type="var">V</span>: <span class="id" type="keyword">Type</span>) := <span class="id" type="var">list</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">V</span>).<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Definition</span> <span class="id" type="var">empty</span> (<span class="id" type="var">V</span>: <span class="id" type="keyword">Type</span>) : <span class="id" type="var">mymap</span> <span class="id" type="var">V</span> := <span class="id" type="var">nil</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">lookup</span> (<span class="id" type="var">V</span>: <span class="id" type="keyword">Type</span>) (<span class="id" type="var">default</span>: <span class="id" type="var">V</span>) (<span class="id" type="var">x</span>: <span class="id" type="var">nat</span>) (<span class="id" type="var">m</span>: <span class="id" type="var">mymap</span> <span class="id" type="var">V</span>) : <span class="id" type="var">V</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">m</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a</span>,<span class="id" type="var">v</span>)::<span class="id" type="var">al</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> =? <span class="id" type="var">a</span> <span class="id" type="keyword">then</span> <span class="id" type="var">v</span> <span class="id" type="keyword">else</span> <span class="id" type="var">lookup</span> <span class="id" type="var">V</span> <span class="id" type="var">default</span> <span class="id" type="var">x</span> <span class="id" type="var">al</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">nil</span> ⇒ <span class="id" type="var">default</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Theorem</span> <span class="id" type="var">lookup_empty</span> (<span class="id" type="var">V</span>: <span class="id" type="keyword">Type</span>) (<span class="id" type="var">default</span>: <span class="id" type="var">V</span>):<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">x</span>, <span class="id" type="var">lookup</span> <span class="id" type="var">V</span> <span class="id" type="var">default</span> <span class="id" type="var">x</span> (<span class="id" type="var">empty</span> <span class="id" type="var">V</span>) = <span class="id" type="var">default</span>.<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">SectionExample1</span>.<br/>
</div>

<div class="doc">
It sure is tedious to repeat the <span class="inlinecode"><span class="id" type="var">V</span></span> and <span class="inlinecode"><span class="id" type="var">default</span></span> parameters
     in every definition and every theorem.  The <span class="inlinecode"><span class="id" type="keyword">Section</span></span> feature
     allows us to declare them as parameters to every definition
     and theorem in the entire section: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">SectionExample2</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Section</span> <span class="id" type="var">MAPS</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Variable</span> <span class="id" type="var">V</span> : <span class="id" type="keyword">Type</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Variable</span> <span class="id" type="var">default</span>: <span class="id" type="var">V</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="id" type="keyword">Definition</span> <span class="id" type="var">mymap</span>  := <span class="id" type="var">list</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">V</span>).<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Definition</span> <span class="id" type="var">empty</span> : <span class="id" type="var">mymap</span> := <span class="id" type="var">nil</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">lookup</span> (<span class="id" type="var">x</span>: <span class="id" type="var">nat</span>) (<span class="id" type="var">m</span>: <span class="id" type="var">mymap</span>) : <span class="id" type="var">V</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">m</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a</span>,<span class="id" type="var">v</span>)::<span class="id" type="var">al</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> =? <span class="id" type="var">a</span> <span class="id" type="keyword">then</span> <span class="id" type="var">v</span> <span class="id" type="keyword">else</span> <span class="id" type="var">lookup</span> <span class="id" type="var">x</span> <span class="id" type="var">al</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">nil</span> ⇒ <span class="id" type="var">default</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Theorem</span> <span class="id" type="var">lookup_empty</span>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">x</span>, <span class="id" type="var">lookup</span> <span class="id" type="var">x</span> <span class="id" type="var">empty</span> = <span class="id" type="var">default</span>.<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">End</span> <span class="id" type="var">MAPS</span>.<br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">SectionExample2</span>.<br/>
</div>

<div class="doc">
At the close of the section, this produces exactly the same
     result:  the functions that "need" to be parametrized by
     <span class="inlinecode"><span class="id" type="var">V</span></span> or <span class="inlinecode"><span class="id" type="var">default</span></span> are given extra parameters.  We can test
     this claim, as follows: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Goal</span> <span class="id" type="var">SectionExample1.empty</span> = <span class="id" type="var">SectionExample2.empty</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Goal</span> <span class="id" type="var">SectionExample1.lookup</span> = <span class="id" type="var">SectionExample2.lookup</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">SectionExample1.lookup</span>, <span class="id" type="var">SectionExample2.lookup</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>. <span class="comment">(*&nbsp;doesn't&nbsp;do&nbsp;anything.&nbsp;*)</span><br/>
</div>

<div class="doc">
Well, not exactly the same; but certainly equivalent.
   Functions <span class="inlinecode"><span class="id" type="var">f</span></span> and <span class="inlinecode"><span class="id" type="var">g</span></span> are "extensionally equal" if, for every
   argument <span class="inlinecode"><span class="id" type="var">x</span></span>, <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">g</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>.  The Axiom of Extensionality
   says that if two functions are "extensionally equal" then they
   are <i>equal</i>.  The <span class="inlinecode"><span class="id" type="tactic">extensionality</span></span> tactic is just a convenient
   way of applying the axiom of extensionality. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">extensionality</span> <span class="id" type="var">V</span>; <span class="id" type="tactic">extensionality</span> <span class="id" type="var">default</span>; <span class="id" type="tactic">extensionality</span> <span class="id" type="var">x</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">extensionality</span> <span class="id" type="var">m</span>; <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">m</span> <span class="id" type="keyword">as</span> [| [? ?] ]; <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">x</span>=?<span class="id" type="var">n</span>); <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab61"></a><h1 class="section">Program for Binary Search Trees</h1>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Section</span> <span class="id" type="var">TREES</span>.<br/>
<span class="id" type="keyword">Variable</span> <span class="id" type="var">V</span> : <span class="id" type="keyword">Type</span>.<br/>
<span class="id" type="keyword">Variable</span> <span class="id" type="var">default</span>: <span class="id" type="var">V</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">key</span> := <span class="id" type="var">nat</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">tree</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;| <span class="id" type="var">E</span> : <span class="id" type="var">tree</span><br/>
&nbsp;| <span class="id" type="var">T</span>: <span class="id" type="var">tree</span> → <span class="id" type="var">key</span> → <span class="id" type="var">V</span> → <span class="id" type="var">tree</span> → <span class="id" type="var">tree</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">empty_tree</span> : <span class="id" type="var">tree</span> := <span class="id" type="var">E</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">lookup</span> (<span class="id" type="var">x</span>: <span class="id" type="var">key</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">tree</span>) : <span class="id" type="var">V</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E</span> ⇒ <span class="id" type="var">default</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T</span> <span class="id" type="var">tl</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">tr</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> &lt;? <span class="id" type="var">k</span> <span class="id" type="keyword">then</span> <span class="id" type="var">lookup</span> <span class="id" type="var">x</span> <span class="id" type="var">tl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="keyword">if</span> <span class="id" type="var">k</span> &lt;? <span class="id" type="var">x</span> <span class="id" type="keyword">then</span> <span class="id" type="var">lookup</span> <span class="id" type="var">x</span> <span class="id" type="var">tr</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">v</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">insert</span> (<span class="id" type="var">x</span>: <span class="id" type="var">key</span>) (<span class="id" type="var">v</span>: <span class="id" type="var">V</span>) (<span class="id" type="var">s</span>: <span class="id" type="var">tree</span>) : <span class="id" type="var">tree</span> :=<br/>
&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">s</span> <span class="id" type="keyword">with</span><br/>
&nbsp;| <span class="id" type="var">E</span> ⇒ <span class="id" type="var">T</span> <span class="id" type="var">E</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span> <span class="id" type="var">E</span><br/>
&nbsp;| <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">y</span> <span class="id" type="var">v'</span> <span class="id" type="var">b</span> ⇒ <span class="id" type="keyword">if</span>  <span class="id" type="var">x</span> &lt;? <span class="id" type="var">y</span> <span class="id" type="keyword">then</span> <span class="id" type="var">T</span> (<span class="id" type="var">insert</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span> <span class="id" type="var">a</span>) <span class="id" type="var">y</span> <span class="id" type="var">v'</span> <span class="id" type="var">b</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="keyword">if</span> <span class="id" type="var">y</span> &lt;? <span class="id" type="var">x</span> <span class="id" type="keyword">then</span> <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">y</span> <span class="id" type="var">v'</span> (<span class="id" type="var">insert</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span> <span class="id" type="var">b</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">x</span> <span class="id" type="var">v</span> <span class="id" type="var">b</span><br/>
&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">elements'</span> (<span class="id" type="var">s</span>: <span class="id" type="var">tree</span>) (<span class="id" type="var">base</span>: <span class="id" type="var">list</span> (<span class="id" type="var">key</span>*<span class="id" type="var">V</span>)) : <span class="id" type="var">list</span> (<span class="id" type="var">key</span> * <span class="id" type="var">V</span>) :=<br/>
&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">s</span> <span class="id" type="keyword">with</span><br/>
&nbsp;| <span class="id" type="var">E</span> ⇒ <span class="id" type="var">base</span><br/>
&nbsp;| <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">b</span> ⇒ <span class="id" type="var">elements'</span> <span class="id" type="var">a</span> ((<span class="id" type="var">k</span>,<span class="id" type="var">v</span>) :: <span class="id" type="var">elements'</span> <span class="id" type="var">b</span> <span class="id" type="var">base</span>)<br/>
&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">elements</span> (<span class="id" type="var">s</span>: <span class="id" type="var">tree</span>) : <span class="id" type="var">list</span> (<span class="id" type="var">key</span> * <span class="id" type="var">V</span>) := <span class="id" type="var">elements'</span> <span class="id" type="var">s</span> <span class="id" type="var">nil</span>.<br/>
</div>

<div class="doc">
<a name="lab62"></a><h1 class="section">Search Tree Examples</h1>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Section</span> <span class="id" type="var">EXAMPLES</span>.<br/>
<span class="id" type="keyword">Variables</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span> : <span class="id" type="var">V</span>.<br/>
<span class="id" type="keyword">Eval</span> <span class="id" type="tactic">compute</span> <span class="id" type="keyword">in</span> <span class="id" type="var">insert</span> 5 <span class="id" type="var">v<sub>5</sub></span> (<span class="id" type="var">insert</span> 2 <span class="id" type="var">v<sub>2</sub></span> (<span class="id" type="var">insert</span> 4 <span class="id" type="var">v<sub>5</sub></span> <span class="id" type="var">empty_tree</span>)).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;T&nbsp;(T&nbsp;E&nbsp;2&nbsp;v<sub>2</sub>&nbsp;E)&nbsp;4&nbsp;v<sub>5</sub>&nbsp;(T&nbsp;E&nbsp;5&nbsp;v<sub>5</sub>&nbsp;E)&nbsp;*)</span><br/>
<span class="id" type="keyword">Eval</span> <span class="id" type="tactic">compute</span> <span class="id" type="keyword">in</span> <span class="id" type="var">lookup</span> 5 (<span class="id" type="var">T</span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 2 <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">E</span>) 4 <span class="id" type="var">v<sub>5</sub></span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 5 <span class="id" type="var">v<sub>5</sub></span> <span class="id" type="var">E</span>)).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;v<sub>5</sub>&nbsp;*)</span><br/>
<span class="id" type="keyword">Eval</span> <span class="id" type="tactic">compute</span> <span class="id" type="keyword">in</span> <span class="id" type="var">lookup</span> 3 (<span class="id" type="var">T</span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 2 <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">E</span>) 4 <span class="id" type="var">v<sub>5</sub></span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 5 <span class="id" type="var">v<sub>5</sub></span> <span class="id" type="var">E</span>)).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;default&nbsp;*)</span><br/>
<span class="id" type="keyword">Eval</span> <span class="id" type="tactic">compute</span> <span class="id" type="keyword">in</span> <span class="id" type="var">elements</span> (<span class="id" type="var">T</span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 2 <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">E</span>) 4 <span class="id" type="var">v<sub>5</sub></span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 5 <span class="id" type="var">v<sub>5</sub></span> <span class="id" type="var">E</span>)).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;<span class="inlinecode">(2,</span> <span class="inlinecode"><span class="id" type="var">v<sub>2</sub></span>);</span> <span class="inlinecode">(4,</span> <span class="inlinecode"><span class="id" type="var">v<sub>5</sub></span>);</span> <span class="inlinecode">(5,</span> <span class="inlinecode"><span class="id" type="var">v<sub>5</sub></span>)</span>&nbsp;*)</span><br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">EXAMPLES</span>.<br/>
</div>

<div class="doc">
<a name="lab63"></a><h1 class="section">What Should We Prove About Search trees?</h1>

<div class="paragraph"> </div>

 Search trees are meant to be an implementation of maps.
   That is, they have an <span class="inlinecode"><span class="id" type="var">insert</span></span> function that corresponds to the
   <span class="inlinecode"><span class="id" type="var">update</span></span> function of a map, and a <span class="inlinecode"><span class="id" type="var">lookup</span></span> function that
   corresponds to applying the map to an argument.  To prove the
   correctness of a search-tree algorithm, we can prove:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Any search tree corresponds to some map, using a function or
         relation that we demonstrate.

</li>
<li> The lookup function gives the same result as applying the map

</li>
<li> The insert function returns a corresponding map.

</li>
<li> Maps have the properties we actually wanted.  It would do no
     good to prove that searchtrees correspond to some abstract
     type X, if X didn't have useful properties!

</li>
</ul>

<div class="paragraph"> </div>

  What properties do we want searchtrees to have?  If I insert
  the binding <span class="inlinecode">(<span class="id" type="var">k</span>,<span class="id" type="var">v</span>)</span> into a searchtree <span class="inlinecode"><span class="id" type="var">t</span></span>, then look up <span class="inlinecode"><span class="id" type="var">k</span></span>, I
  should get <span class="inlinecode"><span class="id" type="var">v</span></span>. If I look up <span class="inlinecode"><span class="id" type="var">k'</span></span> in <span class="inlinecode"><span class="id" type="var">insert</span></span> <span class="inlinecode">(<span class="id" type="var">k</span>,<span class="id" type="var">v</span>)</span> <span class="inlinecode"><span class="id" type="var">t</span></span>, where <span class="inlinecode"><span class="id" type="var">k'</span>≠<span class="id" type="var">k</span></span>,
  then I should get the same result as <span class="inlinecode"><span class="id" type="var">lookup</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span>.  There are several
  more properties. Fortunately, all these properties are already proved
  about <span class="inlinecode"><span class="id" type="var">total_map</span></span> in the <span class="inlinecode"><span class="id" type="var">Maps</span></span> module: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">t_update_eq</span>. <span class="comment">(*&nbsp;&nbsp;:&nbsp;forall&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(m&nbsp;:&nbsp;total_map&nbsp;A)&nbsp;(x&nbsp;:&nbsp;id)&nbsp;(v&nbsp;:&nbsp;A),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t_update&nbsp;m&nbsp;x&nbsp;v&nbsp;x&nbsp;=&nbsp;v&nbsp;&nbsp;&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">t_update_neq</span>. <span class="comment">(*&nbsp;:&nbsp;forall&nbsp;(X&nbsp;:&nbsp;Type)&nbsp;(v&nbsp;:&nbsp;X)&nbsp;(x<sub>1</sub>&nbsp;x<sub>2</sub>&nbsp;:&nbsp;id)&nbsp;(m&nbsp;:&nbsp;total_map&nbsp;X),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;x<sub>1</sub>&nbsp;&lt;&gt;&nbsp;x<sub>2</sub>&nbsp;-&gt;&nbsp;t_update&nbsp;m&nbsp;x<sub>1</sub>&nbsp;v&nbsp;x<sub>2</sub>&nbsp;=&nbsp;m&nbsp;x<sub>2</sub>&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">t_update_shadow</span>. <span class="comment">(*&nbsp;:&nbsp;forall&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(m&nbsp;:&nbsp;total_map&nbsp;A)&nbsp;(v<sub>1</sub>&nbsp;v<sub>2</sub>&nbsp;:&nbsp;A)&nbsp;(x&nbsp;:&nbsp;id),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t_update&nbsp;(t_update&nbsp;m&nbsp;x&nbsp;v<sub>1</sub>)&nbsp;x&nbsp;v<sub>2</sub>&nbsp;=&nbsp;t_update&nbsp;m&nbsp;x&nbsp;v<sub>2</sub>&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">t_update_same</span>. <span class="comment">(*&nbsp;:&nbsp;forall&nbsp;(X&nbsp;:&nbsp;Type)&nbsp;(x&nbsp;:&nbsp;id)&nbsp;(m&nbsp;:&nbsp;total_map&nbsp;X),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t_update&nbsp;m&nbsp;x&nbsp;(m&nbsp;x)&nbsp;=&nbsp;m&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">t_update_permute</span>. <span class="comment">(*&nbsp;forall&nbsp;(X&nbsp;:&nbsp;Type)&nbsp;(v<sub>1</sub>&nbsp;v<sub>2</sub>&nbsp;:&nbsp;X)&nbsp;(x<sub>1</sub>&nbsp;x<sub>2</sub>&nbsp;:&nbsp;id)&nbsp;(m&nbsp;:&nbsp;total_map&nbsp;X),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;x<sub>2</sub>&nbsp;&lt;&gt;&nbsp;x<sub>1</sub>&nbsp;-&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t_update&nbsp;(t_update&nbsp;m&nbsp;x<sub>2</sub>&nbsp;v<sub>2</sub>)&nbsp;x<sub>1</sub>&nbsp;v<sub>1</sub>&nbsp;=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t_update&nbsp;(t_update&nbsp;m&nbsp;x<sub>1</sub>&nbsp;v<sub>1</sub>)&nbsp;x<sub>2</sub>&nbsp;v<sub>2</sub>&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">t_apply_empty</span>. <span class="comment">(*&nbsp;:&nbsp;forall&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(x&nbsp;:&nbsp;id)&nbsp;(v&nbsp;:&nbsp;A),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t_empty&nbsp;v&nbsp;x&nbsp;=&nbsp;v&nbsp;*)</span><br/>
</div>

<div class="doc">
So, if we like those properties that <span class="inlinecode"><span class="id" type="var">total_map</span></span> is proved to have,
   and we can prove that searchtrees behave like maps, then we don't
   have to reprove each individual property about searchtrees.

<div class="paragraph"> </div>

   More generally:  a job worth doing is worth doing well.
   It does no good to prove the "correctness" of a program, if you
   prove that it satisfies a wrong or useless specification. 
<div class="paragraph"> </div>

<a name="lab64"></a><h1 class="section">Efficiency of Search Trees</h1>

<div class="paragraph"> </div>

 We use binary search trees because they are efficient.  That is,
     if there are <span class="inlinecode"><span class="id" type="var">N</span></span> elements in a (reasonably well balanced) BST,
     each insertion or lookup takes about logN time.

<div class="paragraph"> </div>

     What could go wrong?

<div class="paragraph"> </div>

     1.  The search tree might not be balanced.  In that case, each
           insertion or lookup will take as much as linear time.
	   - SOLUTION: use an algorithm, such as "red-black trees",
	   that ensures the trees stay balanced.  We'll do that in
           Chapter <a href="RedBlack.html"><span class="inlineref">RedBlack</span></a>.

<div class="paragraph"> </div>

     2.  Our keys are natural numbers, and Coq's <span class="inlinecode"><span class="id" type="var">nat</span></span> type takes
           linear time <i>per comparison</i>.  That is, computing (j &lt;? k)
           takes time proportional to the <i>value</i> of <span class="inlinecode"><span class="id" type="var">k</span>-<span class="id" type="var">j</span></span>.
	   - SOLUTION: represent keys by a data type that has a more
           efficient comparison operator.  We just use <span class="inlinecode"><span class="id" type="var">nat</span></span> in this
           chapter because it's something you're already familiar with.

<div class="paragraph"> </div>

     3.  There's no notion of "run time" in Coq.  That is, we can't
          say what it means that a Coq function "takes N steps to
          evaluate."  Therefore, we can't prove that binary search
          trees are efficient.
	  - SOLUTION 1: Don't prove (in Coq) that they're efficient;
          just prove that they are correct.  Prove things about their
          efficiency the old-fashioned way, on pencil and paper.
	  - SOLUTION 2: Prove in Coq some facts about the height of
          the trees, which have direct bearing on their efficiency.
          We'll explore that in later chapters.

<div class="paragraph"> </div>

      4.  Our functions in Coq aren't real implementations; they are
          just pretend models of real implementations.  What if there
          are bugs in the correspondence between the Coq function and
          the real implementation?

<div class="paragraph"> </div>

<ul class="doclist">
<li> SOLUTION: Use Coq's <span class="inlinecode"><span class="id" type="var">extraction</span></span> feature to derive the
	    real implementation (in Ocaml or Haskell) automatically
	    from the Coq function.  Or, use Coq's <span class="inlinecode"><span class="id" type="var">vm_compute</span></span> or
	    <span class="inlinecode"><span class="id" type="var">native_compute</span></span> feature to compile and run the programs
	    efficiently inside Coq.  We'll explore <span class="inlinecode"><span class="id" type="var">extraction</span></span> in a
	    later chapter. 
</li>
</ul>

<div class="paragraph"> </div>

<a name="lab65"></a><h1 class="section">Proof of Correctness</h1>

<div class="paragraph"> </div>

 We claim that a <span class="inlinecode"><span class="id" type="var">tree</span></span> "corresponds" to a <span class="inlinecode"><span class="id" type="var">total_map</span></span>.
     So we must exhibit an "abstraction relation"
     <span class="inlinecode"><span class="id" type="var">Abs</span>:</span> <span class="inlinecode"><span class="id" type="var">tree</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">total_map</span></span> <span class="inlinecode"><span class="id" type="var">V</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>.

<div class="paragraph"> </div>

    The idea is that <span class="inlinecode"><span class="id" type="var">Abs</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> says that tree <span class="inlinecode"><span class="id" type="var">t</span></span>
    is a representation of map <span class="inlinecode"><span class="id" type="var">m</span></span>; or that map <span class="inlinecode"><span class="id" type="var">m</span></span>
    is an abstraction of tree <span class="inlinecode"><span class="id" type="var">t</span></span>.  How should we
    define this abstraction relation?

<div class="paragraph"> </div>

    The empty tree is easy:   <span class="inlinecode"><span class="id" type="var">Abs</span></span> <span class="inlinecode"><span class="id" type="var">E</span></span> <span class="inlinecode">(<span class="id" type="keyword">fun</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" type="var">default</span>)</span>.

<div class="paragraph"> </div>

    Now, what about this tree?: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">example_tree</span> (<span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span> : <span class="id" type="var">V</span>) :=<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">T</span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 2 <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">E</span>) 4 <span class="id" type="var">v<sub>4</sub></span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 5 <span class="id" type="var">v<sub>5</sub></span> <span class="id" type="var">E</span>).<br/>
</div>

<div class="doc">
<a name="lab66"></a><h4 class="section">Exercise: 2 stars (example_map)</h4>

</div>
<div class="code code-space">
<span class="comment">(*&nbsp;Fill&nbsp;in&nbsp;the&nbsp;definition&nbsp;of&nbsp;example_map&nbsp;with&nbsp;a&nbsp;total_map&nbsp;that<br/>
&nbsp;&nbsp;you&nbsp;think&nbsp;example_tree&nbsp;should&nbsp;correspond&nbsp;to.&nbsp;&nbsp;Use<br/>
&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="var">t_update</span></span>&nbsp;and&nbsp;<span class="inlinecode">(<span class="id" type="var">t_empty</span></span> <span class="inlinecode"><span class="id" type="var">default</span>)</span>.&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">example_map</span> (<span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>: <span class="id" type="var">V</span>) : <span class="id" type="var">total_map</span> <span class="id" type="var">V</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 To build the <span class="inlinecode"><span class="id" type="var">Abs</span></span> relation, we'll use these two auxiliary
     functions that construct maps: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">combine</span> {<span class="id" type="var">A</span>} (<span class="id" type="var">pivot</span>: <span class="id" type="var">key</span>) (<span class="id" type="var">m<sub>1</sub></span> <span class="id" type="var">m<sub>2</sub></span>: <span class="id" type="var">total_map</span> <span class="id" type="var">A</span>) : <span class="id" type="var">total_map</span> <span class="id" type="var">A</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> &lt;? <span class="id" type="var">pivot</span>  <span class="id" type="keyword">then</span> <span class="id" type="var">m<sub>1</sub></span> <span class="id" type="var">x</span> <span class="id" type="keyword">else</span> <span class="id" type="var">m<sub>2</sub></span> <span class="id" type="var">x</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">combine</span></span> <span class="inlinecode"><span class="id" type="var">pivot</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> uses the map <span class="inlinecode"><span class="id" type="var">a</span></span> on any input less than
   <span class="inlinecode"><span class="id" type="var">pivot</span></span>, and uses map <span class="inlinecode"><span class="id" type="var">b</span></span> on any input <span class="inlinecode"></span> <span class="inlinecode">≥</span> <span class="inlinecode"><span class="id" type="var">pivot</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">Abs</span>:  <span class="id" type="var">tree</span> → <span class="id" type="var">total_map</span> <span class="id" type="var">V</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">Abs_E</span>: <span class="id" type="var">Abs</span> <span class="id" type="var">E</span> (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>)<br/>
| <span class="id" type="var">Abs_T</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">a</span> <span class="id" type="var">b</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">l</span> <span class="id" type="var">a</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">r</span> <span class="id" type="var">b</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> (<span class="id" type="var">T</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span>)  (<span class="id" type="var">t_update</span> (<span class="id" type="var">combine</span> <span class="id" type="var">k</span> <span class="id" type="var">a</span> <span class="id" type="var">b</span>) <span class="id" type="var">k</span> <span class="id" type="var">v</span>).<br/>
</div>

<div class="doc">
<a name="lab67"></a><h4 class="section">Exercise: 3 stars (check_example_map)</h4>
 Prove that your <span class="inlinecode"><span class="id" type="var">example_map</span></span> is the right one.
     If it isn't, go back and fix your definition of <span class="inlinecode"><span class="id" type="var">example_map</span></span>.
     You will probably need the <span class="inlinecode"><span class="id" type="var">bdestruct</span></span> tactic, and <span class="inlinecode"><span class="id" type="tactic">omega</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">check_example_map</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>, <span class="id" type="var">Abs</span> (<span class="id" type="var">example_tree</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>) (<span class="id" type="var">example_map</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">example_tree</span>.<br/>
<span class="id" type="var">evar</span> (<span class="id" type="var">m</span>: <span class="id" type="var">total_map</span> <span class="id" type="var">V</span>).<br/>
<span class="id" type="tactic">replace</span> (<span class="id" type="var">example_map</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>) <span class="id" type="keyword">with</span> <span class="id" type="var">m</span>; <span class="id" type="tactic">subst</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="tactic">repeat</span> <span class="id" type="var">constructor</span>.<br/>
<span class="id" type="tactic">extensionality</span> <span class="id" type="var">x</span>.<br/>
<span class="comment">(*&nbsp;HINT:<br/>
&nbsp;&nbsp;First,&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="tactic">unfold</span></span> <span class="inlinecode"><span class="id" type="var">example_map</span>,</span> <span class="inlinecode"><span class="id" type="var">t_update</span>,</span> <span class="inlinecode"><span class="id" type="var">combine</span>,</span> <span class="inlinecode"><span class="id" type="var">t_empty</span>,</span> <span class="inlinecode"><span class="id" type="var">beq_id</span>.</span><br/>
&nbsp;&nbsp;Then,&nbsp;repeat&nbsp;the&nbsp;following&nbsp;procedure:&nbsp;&nbsp;If&nbsp;you&nbsp;see&nbsp;something&nbsp;like<br/>
&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="keyword">if</span></span> <span class="inlinecode">4</span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode">...</span>,&nbsp;&nbsp;&nbsp;&nbsp;use&nbsp;the&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" type="var">bdestruct</span></span> <span class="inlinecode">(4</span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">x</span>)</span>.<br/>
&nbsp;&nbsp;If&nbsp;the&nbsp;arithmetic&nbsp;facts&nbsp;above&nbsp;the&nbsp;line&nbsp;can't&nbsp;all&nbsp;be&nbsp;true,&nbsp;use&nbsp;<span class="inlinecode"><span class="id" type="tactic">omega</span></span>.<br/>
&nbsp;&nbsp;If&nbsp;you're&nbsp;too&nbsp;lazy&nbsp;to&nbsp;check&nbsp;for&nbsp;yourself&nbsp;whether&nbsp;they&nbsp;are&nbsp;true,<br/>
&nbsp;&nbsp;&nbsp;use&nbsp;<span class="inlinecode"><span class="id" type="var">bdestruct</span></span> <span class="inlinecode">(4</span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">x</span>);</span> <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="tactic">omega</span></span>.<br/>
*)</span><br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 You can ignore this lemma, unless it fails. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">check_too_clever</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>: <span class="id" type="var">V</span>, <span class="id" type="var">True</span>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="var">evar</span> (<span class="id" type="var">m</span>: <span class="id" type="var">total_map</span> <span class="id" type="var">V</span>).<br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">Abs</span> (<span class="id" type="var">example_tree</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>) <span class="id" type="var">m</span>).<br/>
<span class="id" type="tactic">repeat</span> <span class="id" type="var">constructor</span>.<br/>
(<span class="id" type="var">change</span> <span class="id" type="var">m</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">example_map</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>) <span class="id" type="keyword">in</span> <span class="id" type="var">H</span> || <span class="id" type="tactic">auto</span>);<br/>
<span class="comment">(*&nbsp;auto;&nbsp;*)</span><br/>
<span class="id" type="tactic">fail</span> "Did you use copy-and-paste, from your check_example_map proof,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;into your example_map definition?  If so, very clever.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Please try it again with an example_map definition that<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;you make up from first principles.  Or, to skip that,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;uncomment the (* auto; *) above.".<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">empty_tree_relate</span>: <span class="id" type="var">Abs</span> <span class="id" type="var">empty_tree</span> (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="var">constructor</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab68"></a><h4 class="section">Exercise: 3 stars (lookup_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">lookup_relate</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> ,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> → <span class="id" type="var">lookup</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> =  <span class="id" type="var">cts</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab69"></a><h4 class="section">Exercise: 4 stars (insert_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">insert_relate</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> (<span class="id" type="var">insert</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span>) (<span class="id" type="var">t_update</span> <span class="id" type="var">cts</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab70"></a><h1 class="section">Correctness Proof of the <span class="inlinecode"><span class="id" type="var">elements</span></span> Function</h1>

<div class="paragraph"> </div>

 How should we specify what <span class="inlinecode"><span class="id" type="var">elements</span></span> is supposed to do?
     Well, <span class="inlinecode"><span class="id" type="var">elements</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> returns a list of pairs
     <span class="inlinecode">(<span class="id" type="var">k<sub>1</sub></span>,<span class="id" type="var">v<sub>1</sub></span>);(<span class="id" type="var">k<sub>2</sub></span>;<span class="id" type="var">v<sub>2</sub></span>);...;(<span class="id" type="var">kn</span>,<span class="id" type="var">vn</span>)</span> that ought to correspond to
     the total_map, <span class="inlinecode"><span class="id" type="var">t_update</span></span> <span class="inlinecode">...</span> <span class="inlinecode">(<span class="id" type="var">t_update</span></span> <span class="inlinecode">(<span class="id" type="var">t_update</span></span> <span class="inlinecode">(<span class="id" type="var">t_empty</span></span> <span class="inlinecode"><span class="id" type="var">default</span>)</span>
                     <span class="inlinecode">(<span class="id" type="var">Id</span></span> <span class="inlinecode"><span class="id" type="var">k<sub>1</sub></span>)</span> <span class="inlinecode"><span class="id" type="var">v<sub>1</sub></span>)</span> <span class="inlinecode">(<span class="id" type="var">Id</span></span> <span class="inlinecode"><span class="id" type="var">k<sub>2</sub></span>)</span> <span class="inlinecode"><span class="id" type="var">v<sub>2</sub></span>)</span> <span class="inlinecode">...</span> <span class="inlinecode">(<span class="id" type="var">Id</span></span> <span class="inlinecode"><span class="id" type="var">kn</span>)</span> <span class="inlinecode"><span class="id" type="var">vn</span></span>.

<div class="paragraph"> </div>

    We can formalize this quite easily.  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">list2map</span> (<span class="id" type="var">el</span>: <span class="id" type="var">list</span> (<span class="id" type="var">key</span>*<span class="id" type="var">V</span>)) : <span class="id" type="var">total_map</span> <span class="id" type="var">V</span> :=<br/>
&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">el</span> <span class="id" type="keyword">with</span><br/>
&nbsp;| <span class="id" type="var">nil</span> ⇒ <span class="id" type="var">t_empty</span> <span class="id" type="var">default</span><br/>
&nbsp;| (<span class="id" type="var">i</span>,<span class="id" type="var">v</span>)::<span class="id" type="var">el'</span> ⇒ <span class="id" type="var">t_update</span> (<span class="id" type="var">list2map</span> <span class="id" type="var">el'</span>) <span class="id" type="var">i</span> <span class="id" type="var">v</span><br/>
&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
<a name="lab71"></a><h4 class="section">Exercise: 3 stars (elements_relate_informal)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">elements_relate</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>,  <span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> → <span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">t</span>) = <span class="id" type="var">cts</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
</div>

<div class="doc">
Don't prove this yet.  Instead, explain in your own words, with
   examples, why this must be true.  It's OK if your explanation is
   not a formal proof; it's even OK if your explanation is subtly
   wrong!  Just make it convincing. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;YOUR&nbsp;EXPLANATION&nbsp;HERE&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_elements_relate_informal</span> : <span class="id" type="var">option</span> (<span class="id" type="var">prod</span> <span class="id" type="var">nat</span> <span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Instead of doing a <i>formal</i> proof that <span class="inlinecode"><span class="id" type="var">elements_relate</span></span> is true,
    prove that it's false!  That is, as long as type <span class="inlinecode"><span class="id" type="var">V</span></span> contains at
    least two distinct values. 
<div class="paragraph"> </div>

<a name="lab72"></a><h4 class="section">Exercise: 4 stars (not_elements_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">not_elements_relate</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">v</span>, <span class="id" type="var">v</span> ≠ <span class="id" type="var">default</span> →<br/>
&nbsp;&nbsp;¬ (<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>,  <span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> → <span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">t</span>) = <span class="id" type="var">cts</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">intro</span>.<br/>
<span class="id" type="var">pose</span> (<span class="id" type="var">bogus</span> := <span class="id" type="var">T</span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 3 <span class="id" type="var">v</span> <span class="id" type="var">E</span>) 2 <span class="id" type="var">v</span> <span class="id" type="var">E</span>).<br/>
<span class="id" type="var">pose</span> (<span class="id" type="var">m</span> := <span class="id" type="var">t_update</span> (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>) 2 <span class="id" type="var">v</span>).<br/>
<span class="id" type="var">pose</span> (<span class="id" type="var">m'</span> := <span class="id" type="var">t_update</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">combine</span> 2<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">t_update</span> (<span class="id" type="var">combine</span> 3 (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>) (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>)) 3 <span class="id" type="var">v</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>)) 2 <span class="id" type="var">v</span>).<br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">Paradox</span>: <span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">bogus</span>) = <span class="id" type="var">m</span> ∧ <span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">bogus</span>) ≠ <span class="id" type="var">m</span>).<br/>
<span class="id" type="tactic">split</span>.<br/>
</div>

<div class="doc">
To prove the first subgoal, prove that <span class="inlinecode"><span class="id" type="var">m</span>=<span class="id" type="var">m'</span></span> (by <span class="inlinecode"><span class="id" type="tactic">extensionality</span></span>) and
      then use <span class="inlinecode"><span class="id" type="var">H</span></span>.

<div class="paragraph"> </div>

     To prove the second subgoal, do an <span class="inlinecode"><span class="id" type="tactic">intro</span></span> so that you can assume
      <span class="inlinecode"><span class="id" type="var">update_list</span></span> <span class="inlinecode">(<span class="id" type="var">t_empty</span></span> <span class="inlinecode"><span class="id" type="var">default</span>)</span> <span class="inlinecode">(<span class="id" type="var">elements</span></span> <span class="inlinecode"><span class="id" type="var">bogus</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>, then show that
      <span class="inlinecode"><span class="id" type="var">update_list</span></span> <span class="inlinecode">(<span class="id" type="var">t_empty</span></span> <span class="inlinecode"><span class="id" type="var">default</span>)</span> <span class="inlinecode">(<span class="id" type="var">elements</span></span> <span class="inlinecode"><span class="id" type="var">bogus</span>)</span> <span class="inlinecode">(<span class="id" type="var">Id</span></span> <span class="inlinecode">3)</span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">(<span class="id" type="var">Id</span></span> <span class="inlinecode">3)</span>.
      That's a contradiction.

<div class="paragraph"> </div>

      To prove the third subgoal, just destruct <span class="inlinecode"><span class="id" type="var">Paradox</span></span> and use the
      contradiction.

<div class="paragraph"> </div>

      In all 3 goals, when you need to unfold local definitions such
      as <span class="inlinecode"><span class="id" type="var">bogus</span></span> you can use <span class="inlinecode"><span class="id" type="tactic">unfold</span></span> <span class="inlinecode"><span class="id" type="var">bogus</span></span> or <span class="inlinecode"><span class="id" type="tactic">subst</span></span> <span class="inlinecode"><span class="id" type="var">bogus</span></span>.  
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 What went wrong?  Clearly, <span class="inlinecode"><span class="id" type="var">elements_relate</span></span> is true; you just
    explained why.  And clearly, it's not true, because
    <span class="inlinecode"><span class="id" type="var">not_elements_relate</span></span> is provable in Coq.  The problem is that the
    tree <span class="inlinecode">(<span class="id" type="var">T</span></span> <span class="inlinecode">(<span class="id" type="var">T</span></span> <span class="inlinecode"><span class="id" type="var">E</span></span> <span class="inlinecode">3</span> <span class="inlinecode"><span class="id" type="var">v</span></span> <span class="inlinecode"><span class="id" type="var">E</span>)</span> <span class="inlinecode">2</span> <span class="inlinecode"><span class="id" type="var">v</span></span> <span class="inlinecode"><span class="id" type="var">E</span>)</span> is bogus: it's not a well-formed
    binary search tree, because there's a 3 in the left subtree of the
    2 node, and 3 is not less than 2.

<div class="paragraph"> </div>

    If you wrote a good answer to the <span class="inlinecode"><span class="id" type="var">elements_relate_informal</span></span>
    exercise, (that is, an answer that is only subtly wrong), then the
    subtlety is that you assumed that the search tree is well formed.
    That's a reasonable assumption; but we will have to prove that all
    the trees we operate on will be well formed.  
<div class="paragraph"> </div>

<a name="lab73"></a><h1 class="section">Representation Invariants</h1>

<div class="paragraph"> </div>

 A <span class="inlinecode"><span class="id" type="var">tree</span></span> has the <span class="inlinecode"><span class="id" type="var">SearchTree</span></span> property if, at any node with key
     <span class="inlinecode"><span class="id" type="var">k</span></span>, all the keys in the left subtree are less than <span class="inlinecode"><span class="id" type="var">k</span></span>, and all
     the keys in the right subtree are greater than <span class="inlinecode"><span class="id" type="var">k</span></span>.  It's not
     completely obvious how to formalize that!  Here's one way: it's
     correct, but not very practical. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">forall_nodes</span> (<span class="id" type="var">t</span>: <span class="id" type="var">tree</span>) (<span class="id" type="var">P</span>: <span class="id" type="var">tree</span>→<span class="id" type="var">key</span>→<span class="id" type="var">V</span>→<span class="id" type="var">tree</span>→<span class="id" type="keyword">Prop</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;| <span class="id" type="var">E</span> ⇒ <span class="id" type="var">True</span><br/>
&nbsp;| <span class="id" type="var">T</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span> ⇒ <span class="id" type="var">P</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span> ∧ <span class="id" type="var">forall_nodes</span> <span class="id" type="var">l</span> <span class="id" type="var">P</span> ∧ <span class="id" type="var">forall_nodes</span> <span class="id" type="var">r</span> <span class="id" type="var">P</span><br/>
&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">SearchTreeX</span> (<span class="id" type="var">t</span>: <span class="id" type="var">tree</span>) :=<br/>
&nbsp;<span class="id" type="var">forall_nodes</span> <span class="id" type="var">t</span><br/>
&nbsp;&nbsp;&nbsp;(<span class="id" type="keyword">fun</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">forall_nodes</span> <span class="id" type="var">l</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">_</span> <span class="id" type="var">j</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> ⇒ <span class="id" type="var">j</span>&lt;<span class="id" type="var">k</span>) ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">forall_nodes</span> <span class="id" type="var">r</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">_</span> <span class="id" type="var">j</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> ⇒ <span class="id" type="var">j</span>&gt;<span class="id" type="var">k</span>)).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">example_SearchTree_good</span>:<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>, <span class="id" type="var">SearchTreeX</span> (<span class="id" type="var">example_tree</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>4</sub></span> <span class="id" type="var">v<sub>5</sub></span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="var">hnf</span>. <span class="id" type="tactic">simpl</span>.<br/>
<span class="id" type="tactic">repeat</span> <span class="id" type="tactic">split</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">example_SearchTree_bad</span>:<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">v</span>, ¬<span class="id" type="var">SearchTreeX</span> (<span class="id" type="var">T</span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 3 <span class="id" type="var">v</span> <span class="id" type="var">E</span>) 2 <span class="id" type="var">v</span> <span class="id" type="var">E</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">intro</span>.<br/>
<span class="id" type="var">hnf</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="tactic">do</span> 3 <span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">elements_relate_second_attempt</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">SearchTreeX</span> <span class="id" type="var">t</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">t</span>) = <span class="id" type="var">cts</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
</div>

<div class="doc">
This is probably provable.  But the <span class="inlinecode"><span class="id" type="var">SearchTreeX</span></span> property is
   quite unwieldy, with its two Fixpoints nested inside a Fixpoint.
   Instead of using <span class="inlinecode"><span class="id" type="var">SearchTreeX</span></span>, let's reformulate the searchtree
   property as an inductive proposition without any nested
   induction. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Abort</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">SearchTree'</span> : <span class="id" type="var">key</span> → <span class="id" type="var">tree</span> → <span class="id" type="var">key</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">ST_E</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">lo</span> <span class="id" type="var">hi</span>, <span class="id" type="var">lo</span> ≤ <span class="id" type="var">hi</span> → <span class="id" type="var">SearchTree'</span> <span class="id" type="var">lo</span> <span class="id" type="var">E</span> <span class="id" type="var">hi</span><br/>
| <span class="id" type="var">ST_T</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">lo</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span> <span class="id" type="var">hi</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SearchTree'</span> <span class="id" type="var">lo</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SearchTree'</span> (<span class="id" type="var">S</span> <span class="id" type="var">k</span>) <span class="id" type="var">r</span> <span class="id" type="var">hi</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SearchTree'</span> <span class="id" type="var">lo</span> (<span class="id" type="var">T</span> <span class="id" type="var">l</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">r</span>) <span class="id" type="var">hi</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">SearchTree</span>: <span class="id" type="var">tree</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">ST_intro</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span> <span class="id" type="var">hi</span>, <span class="id" type="var">SearchTree'</span> 0 <span class="id" type="var">t</span> <span class="id" type="var">hi</span> → <span class="id" type="var">SearchTree</span> <span class="id" type="var">t</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">SearchTree'_le</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">lo</span> <span class="id" type="var">t</span> <span class="id" type="var">hi</span>, @<span class="id" type="var">SearchTree'</span> <span class="id" type="var">lo</span> <span class="id" type="var">t</span> <span class="id" type="var">hi</span> → <span class="id" type="var">lo</span> ≤ <span class="id" type="var">hi</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">induction</span> 1; <span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Before we prove that <span class="inlinecode"><span class="id" type="var">elements</span></span> is correct, let's consider a simpler version. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">slow_elements</span> (<span class="id" type="var">s</span>: <span class="id" type="var">tree</span>) : <span class="id" type="var">list</span> (<span class="id" type="var">key</span> * <span class="id" type="var">V</span>) :=<br/>
&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">s</span> <span class="id" type="keyword">with</span><br/>
&nbsp;| <span class="id" type="var">E</span> ⇒ <span class="id" type="var">nil</span><br/>
&nbsp;| <span class="id" type="var">T</span> <span class="id" type="var">a</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">b</span> ⇒ <span class="id" type="var">slow_elements</span> <span class="id" type="var">a</span> ++ [(<span class="id" type="var">k</span>,<span class="id" type="var">v</span>)] ++ <span class="id" type="var">slow_elements</span> <span class="id" type="var">b</span><br/>
&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
This one is easier to understand than the <span class="inlinecode"><span class="id" type="var">elements</span></span> function,
    because it doesn't carry the <span class="inlinecode"><span class="id" type="var">base</span></span> list around in its recursion.
    Unfortunately, its running time is quadratic, because at each of
    the <span class="inlinecode"><span class="id" type="var">T</span></span> nodes it does a linear-time list-concatentation.  The
    original <span class="inlinecode"><span class="id" type="var">elements</span></span> function takes linear time overall; that's
    much more efficient.

<div class="paragraph"> </div>

   To prove correctness of <span class="inlinecode"><span class="id" type="var">elements</span></span>, it's actually easier to first
   prove that it's equivalent to <span class="inlinecode"><span class="id" type="var">slow_elements</span></span>, then prove the
   correctness of <span class="inlinecode"><span class="id" type="var">slow_elements</span></span>.  We don't care that <span class="inlinecode"><span class="id" type="var">slow_elements</span></span>
   is quadratic, because we're never going to really run it; it's just
   there to support the proof. 
<div class="paragraph"> </div>

<a name="lab74"></a><h4 class="section">Exercise: 3 stars, optional (elements_slow_elements)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">elements_slow_elements</span>: <span class="id" type="var">elements</span> = <span class="id" type="var">slow_elements</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">extensionality</span> <span class="id" type="var">s</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">elements</span>.<br/>
<span class="id" type="tactic">assert</span> (<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">base</span>, <span class="id" type="var">elements'</span> <span class="id" type="var">s</span> <span class="id" type="var">base</span> = <span class="id" type="var">slow_elements</span> <span class="id" type="var">s</span> ++ <span class="id" type="var">base</span>).<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab75"></a><h4 class="section">Exercise: 3 stars, optional (slow_elements_range)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">slow_elements_range</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">lo</span> <span class="id" type="var">t</span> <span class="id" type="var">hi</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">SearchTree'</span> <span class="id" type="var">lo</span> <span class="id" type="var">t</span> <span class="id" type="var">hi</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> (<span class="id" type="var">k</span>,<span class="id" type="var">v</span>) (<span class="id" type="var">slow_elements</span> <span class="id" type="var">t</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">lo</span> ≤ <span class="id" type="var">k</span> &lt; <span class="id" type="var">hi</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab76"></a><h2 class="section">Auxiliary Lemmas About <span class="inlinecode"><span class="id" type="var">In</span></span> and <span class="inlinecode"><span class="id" type="var">list2map</span></span></h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">In_decidable</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> (<span class="id" type="var">al</span>: <span class="id" type="var">list</span> (<span class="id" type="var">key</span>*<span class="id" type="var">V</span>)) (<span class="id" type="var">i</span>: <span class="id" type="var">key</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span> <span class="id" type="var">v</span>, <span class="id" type="var">In</span> (<span class="id" type="var">i</span>,<span class="id" type="var">v</span>) <span class="id" type="var">al</span>) ∨ (¬<span style='font-size:120%;'>&exist;</span> <span class="id" type="var">v</span>, <span class="id" type="var">In</span> (<span class="id" type="var">i</span>,<span class="id" type="var">v</span>) <span class="id" type="var">al</span>).<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | [<span class="id" type="var">k</span> <span class="id" type="var">v</span>]].<br/>
<span class="id" type="var">right</span>; <span class="id" type="tactic">intros</span> [<span class="id" type="var">w</span> <span class="id" type="var">H</span>]; <span class="id" type="var">inv</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHal</span> <span class="id" type="keyword">as</span> [[<span class="id" type="var">w</span> <span class="id" type="var">H</span>] | <span class="id" type="var">H</span>].<br/>
<span class="id" type="var">left</span>; <span style='font-size:120%;'>&exist;</span> <span class="id" type="var">w</span>; <span class="id" type="var">right</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">k</span> =? <span class="id" type="var">i</span>).<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="var">left</span>; <span class="id" type="tactic">eauto</span>.<br/>
<span style='font-size:120%;'>&exist;</span> <span class="id" type="var">v</span>; <span class="id" type="var">left</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="var">right</span>. <span class="id" type="tactic">intros</span> [<span class="id" type="var">w</span> <span class="id" type="var">H<sub>1</sub></span>].<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="var">inv</span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">eauto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">list2map_app_left</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> (<span class="id" type="var">al</span> <span class="id" type="var">bl</span>: <span class="id" type="var">list</span> (<span class="id" type="var">key</span>*<span class="id" type="var">V</span>)) (<span class="id" type="var">i</span>: <span class="id" type="var">key</span>) <span class="id" type="var">v</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">In</span> (<span class="id" type="var">i</span>,<span class="id" type="var">v</span>) <span class="id" type="var">al</span> → <span class="id" type="var">list2map</span> (<span class="id" type="var">al</span>++<span class="id" type="var">bl</span>) <span class="id" type="var">i</span> = <span class="id" type="var">list2map</span> <span class="id" type="var">al</span> <span class="id" type="var">i</span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="var">revert</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">induction</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [| [<span class="id" type="var">j</span> <span class="id" type="var">w</span>] <span class="id" type="var">al</span>]; <span class="id" type="tactic">intro</span>; <span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="var">inv</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span>. <span class="id" type="var">inv</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">t_update</span>.<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">i</span>=?<span class="id" type="var">i</span>); [ | <span class="id" type="tactic">omega</span>].<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">t_update</span>.<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">j</span>=?<span class="id" type="var">i</span>); <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">list2map_app_right</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> (<span class="id" type="var">al</span> <span class="id" type="var">bl</span>: <span class="id" type="var">list</span> (<span class="id" type="var">key</span>*<span class="id" type="var">V</span>)) (<span class="id" type="var">i</span>: <span class="id" type="var">key</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;~(<span style='font-size:120%;'>&exist;</span> <span class="id" type="var">v</span>, <span class="id" type="var">In</span> (<span class="id" type="var">i</span>,<span class="id" type="var">v</span>) <span class="id" type="var">al</span>) → <span class="id" type="var">list2map</span> (<span class="id" type="var">al</span>++<span class="id" type="var">bl</span>) <span class="id" type="var">i</span> = <span class="id" type="var">list2map</span> <span class="id" type="var">bl</span> <span class="id" type="var">i</span>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="var">revert</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">induction</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [| [<span class="id" type="var">j</span> <span class="id" type="var">w</span>] <span class="id" type="var">al</span>]; <span class="id" type="tactic">intro</span>; <span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">t_update</span>.<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">j</span>=?<span class="id" type="var">i</span>).<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">j</span>.<br/>
<span class="id" type="var">contradiction</span> <span class="id" type="var">H</span>.<br/>
<span style='font-size:120%;'>&exist;</span> <span class="id" type="var">w</span>; <span class="id" type="var">left</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">IHal</span>.<br/>
<span class="id" type="var">contradict</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">u</span> ?].<br/>
<span style='font-size:120%;'>&exist;</span> <span class="id" type="var">u</span>; <span class="id" type="var">right</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">list2map_not_in_default</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> (<span class="id" type="var">al</span>: <span class="id" type="var">list</span> (<span class="id" type="var">key</span>*<span class="id" type="var">V</span>)) (<span class="id" type="var">i</span>: <span class="id" type="var">key</span>),<br/>
&nbsp;&nbsp;&nbsp;~(<span style='font-size:120%;'>&exist;</span> <span class="id" type="var">v</span>, <span class="id" type="var">In</span> (<span class="id" type="var">i</span>,<span class="id" type="var">v</span>) <span class="id" type="var">al</span>) → <span class="id" type="var">list2map</span> <span class="id" type="var">al</span> <span class="id" type="var">i</span> = <span class="id" type="var">default</span>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [| [<span class="id" type="var">j</span> <span class="id" type="var">w</span>] <span class="id" type="var">al</span>].<br/>
<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">simpl</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">t_update</span>.<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">j</span>=?<span class="id" type="var">i</span>).<br/>
<span class="id" type="tactic">subst</span>.<br/>
<span class="id" type="var">contradiction</span> <span class="id" type="var">H</span>.<br/>
<span style='font-size:120%;'>&exist;</span> <span class="id" type="var">w</span>; <span class="id" type="var">left</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">IHal</span>.<br/>
<span class="id" type="tactic">intros</span> [<span class="id" type="var">v</span> ?].<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span style='font-size:120%;'>&exist;</span> <span class="id" type="var">v</span>; <span class="id" type="var">right</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab77"></a><h4 class="section">Exercise: 3 stars, optional (elements_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">elements_relate</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">SearchTree</span> <span class="id" type="var">t</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">t</span>) = <span class="id" type="var">cts</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">elements_slow_elements</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">until</span> 1. <span class="id" type="var">inv</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="var">revert</span> <span class="id" type="var">cts</span>; <span class="id" type="tactic">induction</span> <span class="id" type="var">H<sub>0</sub></span>; <span class="id" type="tactic">intros</span>.<br/>
* <span class="comment">(*&nbsp;ST_E&nbsp;case&nbsp;*)</span><br/>
<span class="id" type="var">inv</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="tactic">reflexivity</span>.<br/>
* <span class="comment">(*&nbsp;ST_T&nbsp;case&nbsp;*)</span><br/>
<span class="id" type="var">inv</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="var">specialize</span> (<span class="id" type="var">IHSearchTree'1</span> <span class="id" type="var">_</span> <span class="id" type="var">H<sub>5</sub></span>). <span class="id" type="tactic">clear</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
<span class="id" type="var">specialize</span> (<span class="id" type="var">IHSearchTree'2</span> <span class="id" type="var">_</span> <span class="id" type="var">H<sub>6</sub></span>). <span class="id" type="tactic">clear</span> <span class="id" type="var">H<sub>6</sub></span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">slow_elements</span>; <span class="id" type="var">fold</span> <span class="id" type="var">slow_elements</span>.<br/>
<span class="id" type="tactic">subst</span>.<br/>
<span class="id" type="tactic">extensionality</span> <span class="id" type="var">i</span>.<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">In_decidable</span> (<span class="id" type="var">slow_elements</span> <span class="id" type="var">l</span>) <span class="id" type="var">i</span>)  <span class="id" type="keyword">as</span> [[<span class="id" type="var">w</span> <span class="id" type="var">H</span>] | <span class="id" type="var">Hleft</span>].<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">list2map_app_left</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">v</span>:=<span class="id" type="var">w</span>); <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="var">pose</span> <span class="id" type="var">proof</span> (<span class="id" type="var">slow_elements_range</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">H0_</span> <span class="id" type="var">H</span>).<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">combine</span>, <span class="id" type="var">t_update</span>.<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">k</span>=?<span class="id" type="var">i</span>); [ <span class="id" type="tactic">omega</span> | ].<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">i</span>&lt;?<span class="id" type="var">k</span>); [ | <span class="id" type="tactic">omega</span>].<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab78"></a><h1 class="section">Preservation of Representation Invariant</h1>

<div class="paragraph"> </div>

 How do we know that all the trees we will encounter (particularly,
  that the <span class="inlinecode"><span class="id" type="var">elements</span></span> function will encounter), have the <span class="inlinecode"><span class="id" type="var">SearchTree</span></span>
  property?  Well, the empty tree is a <span class="inlinecode"><span class="id" type="var">SearchTree</span></span>; and if you insert
  into a tree that's a <span class="inlinecode"><span class="id" type="var">SearchTree</span></span>, then the result is a
  <span class="inlinecode"><span class="id" type="var">SearchTree</span></span>; and these are the only ways that you're supposed to
  build trees.  So we need to prove those two theorems. 
<div class="paragraph"> </div>

<a name="lab79"></a><h4 class="section">Exercise: 1 star (empty_tree_SearchTree)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">empty_tree_SearchTree</span>:  <span class="id" type="var">SearchTree</span> <span class="id" type="var">empty_tree</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">clear</span> <span class="id" type="var">default</span>. <span class="comment">(*&nbsp;This&nbsp;is&nbsp;here&nbsp;to&nbsp;avoid&nbsp;a&nbsp;nasty&nbsp;interaction&nbsp;between&nbsp;Admitted<br/>
&nbsp;&nbsp;&nbsp;and&nbsp;Section/Variable.&nbsp;&nbsp;It's&nbsp;also&nbsp;a&nbsp;hint&nbsp;that&nbsp;the&nbsp;<span class="inlinecode"><span class="id" type="var">default</span></span>&nbsp;value<br/>
&nbsp;&nbsp;&nbsp;is&nbsp;not&nbsp;needed&nbsp;in&nbsp;this&nbsp;theorem.&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab80"></a><h4 class="section">Exercise: 3 stars (insert_SearchTree)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">insert_SearchTree</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">SearchTree</span> <span class="id" type="var">t</span> → <span class="id" type="var">SearchTree</span> (<span class="id" type="var">insert</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">clear</span> <span class="id" type="var">default</span>. <span class="comment">(*&nbsp;This&nbsp;is&nbsp;here&nbsp;to&nbsp;avoid&nbsp;a&nbsp;nasty&nbsp;interaction&nbsp;between&nbsp;Admitted&nbsp;and&nbsp;Section/Variable&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab81"></a><h1 class="section">We Got Lucky</h1>

<div class="paragraph"> </div>

 Recall the statement of <span class="inlinecode"><span class="id" type="var">lookup_relate</span></span>: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">lookup_relate</span>.<br/>
<span class="comment">(*&nbsp;&nbsp;forall&nbsp;(k&nbsp;:&nbsp;key)&nbsp;(t&nbsp;:&nbsp;tree)&nbsp;(cts&nbsp;:&nbsp;total_map&nbsp;V),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Abs&nbsp;t&nbsp;cts&nbsp;-&gt;&nbsp;lookup&nbsp;k&nbsp;t&nbsp;=&nbsp;cts&nbsp;(Id&nbsp;k)&nbsp;&nbsp;*)</span><br/>
</div>

<div class="doc">
In general, to prove that a function satisfies the abstraction relation,
   one also needs to use the representation invariant.  That was certainly
   the case with <span class="inlinecode"><span class="id" type="var">elements_relate</span></span>: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">elements_relate</span>.<br/>
<span class="comment">(*&nbsp;&nbsp;:&nbsp;forall&nbsp;(t&nbsp;:&nbsp;tree)&nbsp;(cts&nbsp;:&nbsp;total_map&nbsp;V),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;SearchTree&nbsp;t&nbsp;-&gt;&nbsp;Abs&nbsp;t&nbsp;cts&nbsp;-&gt;&nbsp;elements_property&nbsp;t&nbsp;cts&nbsp;&nbsp;&nbsp;*)</span><br/>
</div>

<div class="doc">
To put that another way, the general form of <span class="inlinecode"><span class="id" type="var">lookup_relate</span></span> should be: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">lookup_relate'</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> (<span class="id" type="var">k</span> : <span class="id" type="var">key</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">tree</span>) (<span class="id" type="var">cts</span> : <span class="id" type="var">total_map</span> <span class="id" type="var">V</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SearchTree</span> <span class="id" type="var">t</span> → <span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> → <span class="id" type="var">lookup</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> = <span class="id" type="var">cts</span> <span class="id" type="var">k</span>.<br/>
</div>

<div class="doc">
That is certainly provable, since it's a weaker statement than what we proved: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">lookup_relate</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">insert_relate'</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SearchTree</span> <span class="id" type="var">t</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> (<span class="id" type="var">insert</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span>) (<span class="id" type="var">t_update</span> <span class="id" type="var">cts</span> <span class="id" type="var">k</span> <span class="id" type="var">v</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">insert_relate</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The question is, why did we not need the representation invariant in
   the proof of <span class="inlinecode"><span class="id" type="var">lookup_relate</span></span>?  The answer is that our particular Abs
   relation is much more clever than necessary:  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Print</span> <span class="id" type="var">Abs</span>.<br/>
<span class="comment">(*&nbsp;Inductive&nbsp;Abs&nbsp;:&nbsp;tree&nbsp;-&gt;&nbsp;total_map&nbsp;V&nbsp;-&gt;&nbsp;Prop&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;Abs_E&nbsp;:&nbsp;Abs&nbsp;E&nbsp;(t_empty&nbsp;default)<br/>
&nbsp;&nbsp;|&nbsp;Abs_T&nbsp;:&nbsp;forall&nbsp;(a&nbsp;b:&nbsp;total_map&nbsp;V)&nbsp;(l:&nbsp;tree)&nbsp;(k:&nbsp;key)&nbsp;(v:&nbsp;V)&nbsp;(r:&nbsp;tree),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Abs&nbsp;l&nbsp;a&nbsp;-&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Abs&nbsp;r&nbsp;b&nbsp;-&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Abs&nbsp;(T&nbsp;l&nbsp;k&nbsp;v&nbsp;r)&nbsp;(t_update&nbsp;(combine&nbsp;k&nbsp;a&nbsp;b)&nbsp;(Id&nbsp;k)&nbsp;v)<br/>
*)</span><br/>
</div>

<div class="doc">
Because the <span class="inlinecode"><span class="id" type="var">combine</span></span> function is chosen very carefully, it turns out
  that this abstraction relation even works on bogus trees! 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Remark</span> <span class="id" type="var">abstraction_of_bogus_tree</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">v<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">Abs</span> (<span class="id" type="var">T</span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 3 <span class="id" type="var">v<sub>3</sub></span> <span class="id" type="var">E</span>) 2 <span class="id" type="var">v<sub>2</sub></span> <span class="id" type="var">E</span>) (<span class="id" type="var">t_update</span> (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>) 2 <span class="id" type="var">v<sub>2</sub></span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="var">evar</span> (<span class="id" type="var">m</span>: <span class="id" type="var">total_map</span> <span class="id" type="var">V</span>).<br/>
<span class="id" type="tactic">replace</span>  (<span class="id" type="var">t_update</span> (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>) 2 <span class="id" type="var">v<sub>2</sub></span>) <span class="id" type="keyword">with</span> <span class="id" type="var">m</span>; <span class="id" type="tactic">subst</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="tactic">repeat</span> <span class="id" type="var">constructor</span>.<br/>
<span class="id" type="tactic">extensionality</span> <span class="id" type="var">x</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">t_update</span>, <span class="id" type="var">combine</span>, <span class="id" type="var">t_empty</span>.<br/>
<span class="id" type="var">bdestruct</span> (2 =? <span class="id" type="var">x</span>).<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">x</span> &lt;? 2).<br/>
<span class="id" type="var">bdestruct</span> (3 =? <span class="id" type="var">x</span>).<br/>
<span class="comment">(*&nbsp;LOOK&nbsp;HERE!&nbsp;*)</span><br/>
<span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="var">bdestruct</span> (<span class="id" type="var">x</span> &lt;? 3).<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Step through the proof to <span class="inlinecode"><span class="id" type="var">LOOK</span></span> <span class="inlinecode"><span class="id" type="var">HERE</span></span>, and notice what's going on.
   Just when it seems that <span class="inlinecode">(<span class="id" type="var">T</span></span> <span class="inlinecode">(<span class="id" type="var">T</span></span> <span class="inlinecode"><span class="id" type="var">E</span></span> <span class="inlinecode">3</span> <span class="inlinecode"><span class="id" type="var">v<sub>3</sub></span></span> <span class="inlinecode"><span class="id" type="var">E</span>)</span> <span class="inlinecode">2</span> <span class="inlinecode"><span class="id" type="var">v<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">E</span>)</span> is about to produce <span class="inlinecode"><span class="id" type="var">v<sub>3</sub></span></span>
  while <span class="inlinecode">(<span class="id" type="var">t_update</span></span> <span class="inlinecode">(<span class="id" type="var">t_empty</span></span> <span class="inlinecode"><span class="id" type="var">default</span>)</span> <span class="inlinecode">(<span class="id" type="var">Id</span></span> <span class="inlinecode">2)</span> <span class="inlinecode"><span class="id" type="var">v<sub>2</sub></span>)</span> is about to produce <span class="inlinecode"><span class="id" type="var">default</span></span>,
  <span class="inlinecode"><span class="id" type="tactic">omega</span></span> finds a contradiction.  What's happening is that <span class="inlinecode"><span class="id" type="var">combine</span></span> <span class="inlinecode">2</span>
  is careful to ignore any keys &gt;= 2 in the left-hand subtree.

<div class="paragraph"> </div>

  For that reason, <span class="inlinecode"><span class="id" type="var">Abs</span></span> matches the <i>actual</i> behavior of <span class="inlinecode"><span class="id" type="var">lookup</span></span>,
  even on bogus trees.  But that's a really strong condition!  We should
  not have to care about the behavior of <span class="inlinecode"><span class="id" type="var">lookup</span></span> (and <span class="inlinecode"><span class="id" type="var">insert</span></span>) on
  bogus trees.  We should not need to prove anything about it, either.

<div class="paragraph"> </div>

  Sure, it's convenient in this case that the abstraction relation is able to
  cope with ill-formed trees.  But in general, when proving correctness of
  abstract-data-type (ADT) implementations, it may be a lot of extra
  effort to make the abstraction relation as heavy-duty as that.
  It's often much easier for the abstraction relation to assume that the
  representation is well formed.  Thus, the general statement of our
  correctness theorems will be more like <span class="inlinecode"><span class="id" type="var">lookup_relate'</span></span> than like
  <span class="inlinecode"><span class="id" type="var">lookup_relate</span></span>.  
<div class="paragraph"> </div>

<a name="lab82"></a><h1 class="section">Every Well-Formed Tree Does Actually Relate to an Abstraction</h1>

<div class="paragraph"> </div>

 We're not quite done yet.  We would like to know that
    <i>every tree that satisfies the representation invariant, means something</i>.

<div class="paragraph"> </div>

   So as a general sanity check, we need the following theorem: 
<div class="paragraph"> </div>

<a name="lab83"></a><h4 class="section">Exercise: 2 stars (can_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">can_relate</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span>,  <span class="id" type="var">SearchTree</span> <span class="id" type="var">t</span> → <span style='font-size:120%;'>&exist;</span> <span class="id" type="var">cts</span>, <span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Now, because we happen to have a super-strong abstraction relation, that
   even works on bogus trees, we can prove a super-strong can_relate function: 
<div class="paragraph"> </div>

<a name="lab84"></a><h4 class="section">Exercise: 2 stars (unrealistically_strong_can_relate)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">unrealistically_strong_can_relate</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span>,  <span style='font-size:120%;'>&exist;</span> <span class="id" type="var">cts</span>, <span class="id" type="var">Abs</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab85"></a><h1 class="section">It Wasn't Really Luck, Actually</h1>

<div class="paragraph"> </div>

 In the previous section, I said, "we got lucky that the abstraction
    relation that I happened to choose had this super-strong property."

<div class="paragraph"> </div>

    But actually, the first time I tried to prove correctness of search trees,
    I did <i>not</i> get lucky.  I chose a different abstraction relation: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">AbsX</span> (<span class="id" type="var">t</span>: <span class="id" type="var">tree</span>) (<span class="id" type="var">m</span>: <span class="id" type="var">total_map</span> <span class="id" type="var">V</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">t</span>) = <span class="id" type="var">m</span>.<br/>
</div>

<div class="doc">
It's easy to prove that <span class="inlinecode"><span class="id" type="var">elements</span></span> respects this abstraction relation: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">elements_relateX</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">SearchTree</span> <span class="id" type="var">t</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">AbsX</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">t</span>) = <span class="id" type="var">cts</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
But it's not so easy to prove that <span class="inlinecode"><span class="id" type="var">lookup</span></span> and <span class="inlinecode"><span class="id" type="var">insert</span></span> respect this
    relation.  For example, the following claim is not true. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">naive_lookup_relateX</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> ,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AbsX</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> → <span class="id" type="var">lookup</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> =  <span class="id" type="var">cts</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Abort</span>. <span class="comment">(*&nbsp;Not&nbsp;true&nbsp;*)</span><br/>
</div>

<div class="doc">
In fact, <span class="inlinecode"><span class="id" type="var">naive_lookup_relateX</span></span> is provably false,
     as long as the type <span class="inlinecode"><span class="id" type="var">V</span></span> contains at least two different values. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">not_naive_lookup_relateX</span>:<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">v</span>, <span class="id" type="var">default</span> ≠ <span class="id" type="var">v</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;¬ (<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> , <span class="id" type="var">AbsX</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> → <span class="id" type="var">lookup</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> =  <span class="id" type="var">cts</span> <span class="id" type="var">k</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">AbsX</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">v</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="var">pose</span> (<span class="id" type="var">bogus</span> := <span class="id" type="var">T</span> (<span class="id" type="var">T</span> <span class="id" type="var">E</span> 3 <span class="id" type="var">v</span> <span class="id" type="var">E</span>) 2 <span class="id" type="var">v</span> <span class="id" type="var">E</span>).<br/>
<span class="id" type="var">pose</span> (<span class="id" type="var">m</span> := <span class="id" type="var">t_update</span> (<span class="id" type="var">t_update</span> (<span class="id" type="var">t_empty</span> <span class="id" type="var">default</span>) 2 <span class="id" type="var">v</span>) 3 <span class="id" type="var">v</span>).<br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">list2map</span> (<span class="id" type="var">elements</span> <span class="id" type="var">bogus</span>) = <span class="id" type="var">m</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">assert</span> (¬ <span class="id" type="var">lookup</span> 3 <span class="id" type="var">bogus</span> = <span class="id" type="var">m</span> 3). {<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bogus</span>, <span class="id" type="var">m</span>, <span class="id" type="var">t_update</span>, <span class="id" type="var">t_empty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
}<br/>
<span class="comment">(**&nbsp;Right&nbsp;here&nbsp;you&nbsp;see&nbsp;how&nbsp;it&nbsp;is&nbsp;proved.&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="var">bogus</span></span>&nbsp;is&nbsp;our&nbsp;old&nbsp;friend,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;the&nbsp;bogus&nbsp;tree&nbsp;that&nbsp;does&nbsp;not&nbsp;satisfy&nbsp;the&nbsp;<span class="inlinecode"><span class="id" type="var">SearchTree</span></span>&nbsp;property.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="var">m</span></span>&nbsp;is&nbsp;the&nbsp;<span class="inlinecode"><span class="id" type="var">total_map</span></span>&nbsp;that&nbsp;corresponds&nbsp;to&nbsp;the&nbsp;elements&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="var">bogus</span></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;The&nbsp;<span class="inlinecode"><span class="id" type="var">lookup</span></span>&nbsp;function&nbsp;returns&nbsp;<span class="inlinecode"><span class="id" type="var">default</span></span>&nbsp;at&nbsp;key&nbsp;<span class="inlinecode">3</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;but&nbsp;the&nbsp;map&nbsp;<span class="inlinecode"><span class="id" type="var">m</span></span>&nbsp;returns&nbsp;<span class="inlinecode"><span class="id" type="var">v</span></span>&nbsp;at&nbsp;key&nbsp;<span class="inlinecode">3</span>.&nbsp;&nbsp;And&nbsp;yet,&nbsp;assumption&nbsp;<span class="inlinecode"><span class="id" type="var">H<sub>0</sub></span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;claims&nbsp;that&nbsp;they&nbsp;should&nbsp;return&nbsp;the&nbsp;same&nbsp;thing.&nbsp;*)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab86"></a><h4 class="section">Exercise: 4 stars, optional (lookup_relateX)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">lookup_relateX</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> ,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SearchTree</span> <span class="id" type="var">t</span> → <span class="id" type="var">AbsX</span> <span class="id" type="var">t</span> <span class="id" type="var">cts</span> → <span class="id" type="var">lookup</span> <span class="id" type="var">k</span> <span class="id" type="var">t</span> =  <span class="id" type="var">cts</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">AbsX</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>. <span class="id" type="tactic">subst</span> <span class="id" type="var">cts</span>.<br/>
<span class="id" type="var">inv</span> <span class="id" type="var">H</span>. <span class="id" type="var">remember</span> 0 <span class="id" type="keyword">as</span> <span class="id" type="var">lo</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="tactic">clear</span> - <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">elements_slow_elements</span>.<br/>
</div>

<div class="doc">
To prove this, you'll need to use this collection of facts:
   <span class="inlinecode"><span class="id" type="var">In_decidable</span></span>, <span class="inlinecode"><span class="id" type="var">list2map_app_left</span></span>, <span class="inlinecode"><span class="id" type="var">list2map_app_right</span></span>,
   <span class="inlinecode"><span class="id" type="var">list2map_not_in_default</span></span>, <span class="inlinecode"><span class="id" type="var">slow_elements_range</span></span>.  The point is,
   it's not very pretty. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab87"></a><h2 class="section">Coherence With <span class="inlinecode"><span class="id" type="var">elements</span></span> Instead of <span class="inlinecode"><span class="id" type="var">lookup</span></span></h2>
 The first definition of the abstraction relation, <span class="inlinecode"><span class="id" type="var">Abs</span></span>, is "coherent"
     with the <span class="inlinecode"><span class="id" type="var">lookup</span></span> operation, but not very coherent with the <span class="inlinecode"><span class="id" type="var">elements</span></span>
     operation.  That is, <span class="inlinecode"><span class="id" type="var">Abs</span></span> treats all trees, including ill-formed ones,
     much the way <span class="inlinecode"><span class="id" type="var">lookup</span></span> does, so it was easy to prove <span class="inlinecode"><span class="id" type="var">lookup_relate</span></span>.
     But it was harder to prove <span class="inlinecode"><span class="id" type="var">elements_relate</span></span>.

<div class="paragraph"> </div>

    The alternate abstraction relation, <span class="inlinecode"><span class="id" type="var">AbsX</span></span>, is coherent with <span class="inlinecode"><span class="id" type="var">elements</span></span>,
    but not very coherent with <span class="inlinecode"><span class="id" type="var">lookup</span></span>.  So proving <span class="inlinecode"><span class="id" type="var">elements_relateX</span></span> is
    trivial, but proving <span class="inlinecode"><span class="id" type="var">lookup_relate</span></span> is difficult.

<div class="paragraph"> </div>

    This kind of thing comes up frequently.  The important thing to remember
    is that you often have choices in formulating the abstraction relation,
    and the choice you make will affect the simplicity and elegance of your
    proofs.   If you find things getting too difficult, step back and reconsider
    your abstraction relation. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">TREES</span>.<br/>
</div>
</div>



</div>

</body>
</html>